| Definitions | True,  T, ff, P   Q, P  Q, tt, if b then t else f fi , Top, P & Q,   x. t(x), R-Feasible(R), R-size(R), A c B,  , {T}, SQType(T), i  j , False,  A, A  B, P Q, t  T,  x:A. B(x),  , Rnone?(x1), Rplus-right(x1), Rplus-left(x1), Rplus?(x1), Y, A || B, x(s), Unit, Realizer, P  Q, Dec(P),   , , S  T, Rrframe(loc;x;L), Rbframe(loc;k;L), Raframe(loc;k;L), Rpre(loc;ds;a;p;P), Rsends(ds;knd;T;l;dt;g), Reffect(loc;ds;knd;T;x;f), Rsframe(lnk;tag;L), Rframe(loc;T;x;L), Rinit(loc;T;x;v), left  right, Rnone(),  |
| Lemmas | assert of lt int, bnot of le int, squash wf, eqff to assert, bnot wf, lt int wf, assert of le int, eqtt to assert, iff transitivity, nat plus inc, le int wf, ifthenelse wf, R-compat-symmetry, interface-compatible-join2, R-compat-Rplus2, R-compat-implies, interface-compatible-join, Rrframe wf, Rbframe wf, Raframe wf, Rpre wf, lsrc wf, tagof wf, id-deq wf, fpf-cap wf, eq lnk wf, Rsends wf, lnk wf, ldst wf, isrcv wf, normal-ds wf, Reffect wf, Rsframe wf, normal-type wf, Rframe wf, Rinit wf, Rplus wf, R-Dsys-Rplus, true wf, Rnone wf, not wf, bool wf, finite-prob-space wf, decl-type wf, decl-state wf, fpf wf, IdLnk wf, Knd wf, rationals wf, Id wf, unit wf, decidable le, R-Feasible wf, R-compat wf, Rplus? wf, assert wf, Rplus-left wf, Rplus-right wf, R-size-decreases, R-interface-base, R-Dsys wf, decidable int equal, es realizer wf, nat plus wf, le wf, R-size wf, ge wf, nat properties, nat wf |